package dbc;

import java.io.IOException;
import java.io.PrintWriter;
import java.util.Set;
import javax.annotation.processing.AbstractProcessor;
import javax.annotation.processing.Filer;
import javax.annotation.processing.RoundEnvironment;
import javax.annotation.processing.SupportedAnnotationTypes;
import javax.annotation.processing.SupportedSourceVersion;
import javax.lang.model.SourceVersion;
import javax.lang.model.element.Element;
import javax.lang.model.element.TypeElement;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Types;
import javax.tools.Diagnostic.Kind;
import javax.tools.StandardLocation;

/**
* InvariantProcessor is called at compilation time to process
* all @Invariant annotations in the source code.
* For each class annoted with @Invariant, this processor will create
* an aspect per class' method which will have to be compile with aspectj.
*/
// InvariantProcessor supports only Invariant annotations
@SupportedAnnotationTypes({"dbc.Invariant"})
// Only Java >= 6 is supported
@SupportedSourceVersion(SourceVersion.RELEASE_6)
public class InvariantProcessor extends AbstractProcessor {
    
    /**
     * Process is called during compilation to parse all @Invariant annotations
     * @param annotations A set containing all @Invariant annotations
     * @param roundEnv Object representating the current step of annotations processing
     * @return true on success
     */
    @Override
    public boolean process(Set<? extends TypeElement> annotations, RoundEnvironment roundEnv) {
	// Creating ressources for output resulting file
        Filer filer = processingEnv.getFiler();
        Types types = processingEnv.getTypeUtils();

	// Get all Elements (here classes) annoted with @Invariant
	// Each Element will be process to create an aspect
        for(Element element : roundEnv.getElementsAnnotatedWith(Invariant.class)) {
            try {
		// Getting usefull informations such as class name to generate an unique aspect name
                TypeMirror classType = element.asType();

                String className = classType.toString();
                String erasedClassName = types.erasure(classType).toString();

                String aspectName = "InvariantAspect_" + erasedClassName;
                aspectName = aspectName.replace(".", "_");

                PrintWriter pw = new PrintWriter(
                        filer.createResource(StandardLocation.SOURCE_OUTPUT,
                                             "aspects", aspectName + ".aj")
                                             .openOutputStream());
		// Here we have the invariant annotation
                Invariant invariant = element.getAnnotation(Invariant.class);
		// Analyzing contract include in invariant.value()
                SyntaxHandler sh = new SyntaxHandler(invariant.value());
                sh.processExpression();
                String condition = sh.getProcessedExpression();

                //Aspect generation
                pw.println("privileged aspect " + aspectName + " implements dbc.Contract {");

                pw.println("private void " + erasedClassName + ".invariantAssert() {");
                pw.println(sh.getGeneratedCode());
                pw.println("if(!(" + condition + ")) {");
                pw.println("throw new dbc.InvariantException(\"Class invariant violated in " + className + "\");");
                pw.println("}");
                pw.println("}");

                pw.println("pointcut constructor(): execution(" + erasedClassName + ".new(..));");
                pw.print("pointcut method(): call(* " + erasedClassName + ".*(..)) && !cflow(constructor())");
                pw.println(" && !this(" + erasedClassName + ") && !within(dbc.Contract+);");

                pw.println("before(" + erasedClassName + " t): method() && target(t) {");
                pw.println("t.invariantAssert();");
                pw.println("}");

                pw.println("after(" + erasedClassName + " t): (method() || constructor()) && target(t) {");
                pw.println("t.invariantAssert();");
                pw.println("}");

                pw.println("}");

                pw.close();


            } catch(IOException ex) {
		// If something goes wrong display a warning and return
                processingEnv.getMessager().printMessage(Kind.WARNING, ex.getMessage());
            }
        }

        return true;
    }
}
